T:Type, eq:EqDecider(T), es:ES, x:Id, e:E.
@loc(e)(x:T)
 (e':E.
 ((x changed before e) c ((last change to x before e) = e'))
  ((e' <loc e)
  & (((x after e') = (x when e')  T))
  & (e'':E. (e' <loc e'')  (e'' <loc e)  ((x after e'') = (x after e')  T)))) 

latex

Definitions	True, T, x. t(x), , P  Q, t  T, (e <loc e'), P & Q, A c B, P  Q, P  Q, x:A. B(x), P  Q, {T}, x(s), WellFnd{i}(A;x,y.R(x;y)), @i(x:T)
Lemmas	es-le weakening, es-locl transitivity2, es-pred-locl, es-pred wf, es-loc-pred, true wf, squash wf, es-locl-wellfnd, es-locl wf, es-locl-iff, es-after-pred2, deq wf, event system wf, es-when wf, es-vartype wf, es-after wf, not wf, es-causl wf, Id wf, last-change wf, es-E wf, es-loc wf, es-dtype wf, changed wf, assert wf, last-change-equal